\begin{tabbing}
$\forall$$T$:Type, ${\it ll}$:($T$ List) List.
\\[0ex]$\neg$concat(${\it ll}$) $=$ nil $\in$ $T$ List
\\[0ex]$\Rightarrow$ (\=$\exists$${\it ll}_{1}$:($T$ List) List, $l_{1}$:$T$ List.\+
\\[0ex]concat(${\it ll}$) $=$ (concat(${\it ll}_{1}$) @ $l_{1}$ @ [last(concat(${\it ll}$))]) $\in$ $T$ List
\\[0ex]\& ${\it ll}_{1}$ @ [$l_{1}$ @ [last(concat(${\it ll}$))]] $\leq$ ${\it ll}$)
\-
\end{tabbing}